$\forall$$R$:es\_realizer\{i:l\}. Rds($R$) $\in$ fpf(Id; $x$.Type)